\begin{tabbing}
$i$ $\parallel$ $a$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Trans($i$):$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$es\_state(${\it es}$;$i$)$\rightarrow$es\_state(${\it es}$;$i$)$\parallel$$a$\+
\\[0ex]\& Send($i$):$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$state@$i$$\rightarrow$(Msg List)$\parallel$$a$
\\[0ex]\& Choose($i$):$b$:Id$\rightarrow\mathbb{N}\rightarrow$state@$i$$\rightarrow$(?kindtype($i$;locl($b$)))$\parallel$$a$
\-
\end{tabbing}